(declare-fun var0 () String)
(declare-fun var1 () String)
(declare-fun var2 () String)
(declare-fun var3 () Int)
(declare-fun var4 () Int)
(declare-fun var5 () Int)
(declare-fun var6 () Bool)
(declare-fun var7 () Bool)
(declare-fun var8 () Bool)
(assert (>= (str.len (str.substr var0 var5 var5)) (str.indexof var0 var2 var4)))
(assert (< (str.indexof var1 "=L7d:h?Fj)" var4) (str.indexof var2 var0 var4)))
(assert (<= (str.len var2) (str.indexof var1 var2 var3)))
(assert (>= (str.indexof (str.replace var0 var2 var1) (str.substr var1 var3 var4) (str.indexof var1 var2 var3)) (str.len "5[f^J-MV2g")))
(check-sat)
